package br.cin.ufpe.rabbit;

import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.search.Search;

import java.util.Comparator;
import java.util.List;

/**
 * class with constants used to configure the
 * extractor of interesting (likely racy) 
 * data-dependencies
 */
public class RabbitConfig {
	
	public enum Distance {METHOD,INSTRUCTION};
	public enum ExecutionMode {DOUBLE,SINGLE};
	public static Distance distance = Distance.METHOD; 
	public static ExecutionMode executionMode = ExecutionMode.DOUBLE;
	
	
	
	public enum PathGenericValue {ARITHMETIC_MEAN,GEOMETRIC_MEAN};//average 
	public static PathGenericValue pathGenericValue = PathGenericValue.GEOMETRIC_MEAN; 
	
	public static boolean LogStates = false;
	
	//String Representation of MethodReturn at call Trace
	public static String ReturnMethodString = "*";
	
	public static boolean DEBUG = false;
	
	/**
	 * comparator used in a tree set implementation. this 
	 * object is shared across different sets.
	 */
	public static Comparator<ElementInfo> comp = new Comparator<ElementInfo>() {
		@Override
		public int compare(ElementInfo o1, ElementInfo o2) {
			int v1 = o1.getIndex(), v2 = o2.getIndex();
			return v1 > v2 ? 1 : v1 < v2 ? -1 : 0;
		}
	};


	/**
	 * JPF identifiers of bytecodes used to 
	 * update the heap.  Note that we do not
	 * consider array accesses yet.
	 */
	public final static int PUTFIELD_opcode = 0xB5;
	public final static int GETFIELD_opcode = 0xB4;
	public final static int PUTSTATIC_opcode = 0xB3;
	public final static int GETSTATIC_opcode = 0xB2;
	
	/**
	 * identifier to use as a mock to an object id.
	 * we want to store accesses to static field
	 * in the same data-structures to store object 
	 * field accesses.
	 */
	public final static int MOCK_CLASS_ID = -2;

	/**
	 * option of report when search finishes
	 */
	public static enum REPORT_OPTION {
		PRINT_RWSETS, PRINT_INTERESTING, PRINT_ALL, NONE
	};
	public static REPORT_OPTION opt = REPORT_OPTION.PRINT_INTERESTING;

	
	/**
	 * aggressive optimization based on the observation
	 * that races rarely occur on setup methods.  
	 */
	public static  boolean IGNORE_INIT = true;
	public static  boolean IGNORE_RUN = true;
	public static  boolean IGNORE_CLINIT = true;
	public static  boolean IGNORE_MAIN = true;

	/**
	 * variable that defines when to top search.
	 * for example, if using Yoshi for inspection
	 * one can stop the search quickly to inspect.
	 * use -1 to ignore this feature.
	 */
	public static final int STOP_AFTER = -1;
	
	
	/**
	 * Time to stop the search
	 */
	public static int TIME_UNTIL_STOP = 5000;

	/**
	 * Controls if potential races will check in runtime or just in the end of search 
	 * */
	public static boolean RUNTIME_CHECK_RACES = false;

	/**
	 * if set this variable will print a dot (".")
	 * for every new state explored.  note that
	 * this should not be used if measuring time.
	 * it significantly slows down execution (due
	 * to the calls to System.out).
	 */
	public static boolean SHOW_PROGRESS = false; 
	
	
	/**
	 * if set this variable will print some information
	 * for every new state explored.  note that
	 * this should not be used if measuring time.
	 * it significantly slows down execution (due
	 * to the calls to System.out).
	 */
	public static boolean SHOW_STATE_GENERATION = false;

	
	/**
	 * if set this variable will print Detailed information
	 * for every new state explored.  note that
	 * this should not be used if measuring time.
	 * it significantly slows down execution (due
	 * to the calls to System.out).
	 */
	public static boolean SHOW_DETAILED_STATE_GENERATION = false;
	
	
	/**
	 * if set this variable will print important
	 * information to avaliate distance of states,
	 * like threads, current methods and heuristic
	 * value
	 */
	public static boolean SHOW_STATE_AVALIATION = true;
	
	
	public static boolean ACTIVATE_STOPPING_CRITERION = true;
	
	/**
	 * Used in tests 
	 * @author elton
	 * 
	 */
	public static boolean TESTING = false;
	public enum Report {DOT,O,F,T,ID,STAR,NO};
	public static List<String> progress;
	public static Report report = Report.DOT;
	
//	static int count = 0;
//	public static void testReport(Search search, Report report) {
//		count++;
//		String signal = reportAsString(report, search);
//		if(TESTING){
//			progress.add(signal);
//		}else{
//			System.out.print(count%80==0?signal+"\n":signal);
//		}
//	}
	public static void testReport(Search search, Report report, int statesAdvanced, boolean addInfo) {
//		count++;
		String info;
		if (addInfo) {
    	info = reportAsString(report, search) +"("+statesAdvanced+")" ;
		}else{
    	info = reportAsString(report, search) ;
    }
		
		if(TESTING){
			progress.add(info);
		}else{
			System.out.print(statesAdvanced%80==0?info+"\n":info);
		}
	}
	
	public static String reportAsString(Report report, Search search){
		String signal;
		switch (report) {
		case DOT:
			signal = ".";	
			break;
		case O:
		case F:
		case T:
			signal = report.toString();
			break;
		case ID:
			signal = Integer.toString(search.getStateId());
			break;
		case STAR:
			signal = "*";
			break;
		case NO:
			signal = "";
			break;
		default://NO
			throw new UnsupportedOperationException("Add " + report + "as signal report");
		}
		return signal;
	}
	
}
